﻿// --------------------------------------------------------------------------------------------------------------------
// <copyright file="A1B1Tree.cs" company="Team Awesome">
//   Awesome
// </copyright>
// <summary>
//   Defines the BinaryTree type.
// </summary>
// --------------------------------------------------------------------------------------------------------------------

namespace System.Collections
{
    using Diagnostics.Contracts;
    using Generic;

	/// <summary>
    /// Uses the standard implementation of a binary tree.
    /// </summary>
    public class A1B1Tree : TreeBase
    {
        /// <summary>
        /// Is true if the tree is a snapshot of another tree.
        /// </summary>
        private readonly bool _isSnapshot;

        /// <summary>
        /// Is true if the tree has been used to make a snapshot.
        /// </summary>
        private bool _hasSnapshot;

        /// <summary>
        /// The root node from which all other nodes can be found.
        /// </summary>
        private BinaryTreeNode _root;

        /// <summary>
        /// Initializes a new instance of the <see cref="A1B1Tree"/> class as a snapshot.
        /// </summary>
        /// <param name="tree">
        /// The tree to create a snapshot from.
        /// </param>
        private A1B1Tree(A1B1Tree tree)
        {
        	Contract.Ensures(_isSnapshot);

            _root = tree._root;
            _isSnapshot = true;
        }

        /// <summary>
        /// Initializes a new instance of the <see cref="A1B1Tree"/> class.
        /// </summary>
        public A1B1Tree()
        {
        }

        #region Implementation of IEnumerable

        /// <summary>
        /// Returns an enumerator that iterates through the collection.
        /// </summary>
        /// <returns>
        /// A <see cref="T:System.Collections.Generic.IEnumerator`1"/> that can be used to iterate through the collection.
        /// </returns>
        /// <filterpriority>1</filterpriority>
        public override IEnumerator<int> GetEnumerator()
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Ensures(Contract.Result<IEnumerator>() != null);
			////Contract.Ensures(CheckConsistency(Contract.Result<IEnumerator<int>>()));

            #endregion
			
			return _root == null ? GetEmptyEnumerator() : GetEnumerator(_root, ChangeStamp);
        }

		/////// <summary>
		/////// *********
		/////// This method has been commented out since it was unusable by the contract for GetEnumerator.
		/////// As mentioned in the report section 6.5 this would change the state of the enumerator.
		/////// 
		/////// Checks if the tree contains all elements from the enumerator and
		/////// if the enumerator is sorted.
		/////// </summary>
		/////// <param name="enumerator">
		/////// The enumerator.
		/////// </param>
		/////// <returns>
		/////// A boolean representing whether the tree contains all elements from the enumerator and
		/////// if the enumerator is sorted.
		/////// </returns>
		////[Pure]
		////private bool CheckConsistency(IEnumerator<int> enumerator)
		////{
		////    var lastItem = int.MinValue;
		////    var en = enumerator;
		////    while (en.MoveNext())
		////    {
		////        Contract.Assert(Contains(enumerator.Current));
		////        Contract.Assert(!(lastItem > enumerator.Current));

		////        lastItem = enumerator.Current;
		////    }
		////    return true;
		////}

    	/// <summary>
    	/// Used when _root is null instead of returning null
    	/// </summary>
    	/// <returns>
    	/// An empty enumerator
    	/// </returns>
    	private static IEnumerator<int> GetEmptyEnumerator()
		{
			yield break;
		}

        /// <summary>
        /// Constructs an enumerator over all children nodes and the node itself ordered.
        /// </summary>
        /// <param name="node">
        /// The node.
        /// </param>
        /// <param name="originalStamp">
        /// The original Stamp.
        /// </param>
        /// <returns>
        /// An enumerator over the items in the tree.
        /// </returns>
        private IEnumerator<int> GetEnumerator(BinaryTreeNode node, int originalStamp)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(ChangeStamp == originalStamp);
        	Contract.Requires(node != null);

            #endregion

            var stack = new Stack<BinaryTreeNode>();
            stack.Push(node);
            BinaryTreeNode lastNode;
            BinaryTreeNode current = null;
            while (stack.Count > 0)
            {
                lastNode = current;
                current = stack.Peek();
                if (current.Left != null && (lastNode == null || lastNode.Item < current.Left.Item))
                {
                    stack.Push(current.Left);
                }
                else
                {
                    CheckModified(originalStamp);
                    yield return stack.Pop().Item;
                    if (current.Right != null)
                        stack.Push(current.Right);
                }
            }
        }

        #endregion

        #region Implementation of ICollection<int>

        /// <summary>
        /// Adds an item to the <see cref="T:System.Collections.Generic.ICollection`1"/>.
        /// </summary>
        /// <param name="item">The object to add to the <see cref="T:System.Collections.Generic.ICollection`1"/>.</param><exception cref="T:System.NotSupportedException">The <see cref="T:System.Collections.Generic.ICollection`1"/> is read-only.</exception>
        public override void Add(int item)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(!IsReadOnly);

            Contract.Ensures(Contains(item));
			Contract.Ensures(item == Contract.OldValue(item));
			Contract.Ensures(_root != null);
            Contract.Ensures(_hasSnapshot == Contract.OldValue(_hasSnapshot));

            #endregion

            var isUpdated = false;
            AddHelper(item, ref isUpdated);
        }

        /// <summary>
        /// Method used, because Code Contracts can't use local variables in postcondition.
        /// </summary>
        /// <param name="item">
        /// The item.
        /// </param>
        /// <param name="isUpdated">
        /// The is Updated.
        /// </param>
        private void AddHelper(int item, ref bool isUpdated)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(!IsReadOnly);
            Contract.Requires(!isUpdated);
            Contract.Ensures(Contains(item));
            Contract.Ensures(item == Contract.OldValue(item));
			////Contract.Ensures(isUpdated ? this.Count == Contract.OldValue(this.Count) + 1 : this.Count == Contract.OldValue(this.Count));
            Contract.Ensures(_hasSnapshot == Contract.OldValue(_hasSnapshot));

            #endregion

            _root = Add(_root, item, ref isUpdated);
        }

        /// <summary>
        /// Takes a node and tests if it should move further down the tree or if it should insert right away.
        /// </summary>
        /// <param name="node">
        /// The node which tree to insert in.
        /// </param>
        /// <param name="item">
        /// The item to insert.
        /// </param>
        /// <param name="isUpdated">
        /// Denotes if the tree has been updated, so in case of the tree having snapshots, the
        /// path should be copied.
        /// </param>
        /// <returns>
        /// The node which possibly has the item inserted in it or some node in its subtree.
        /// </returns>
        private BinaryTreeNode Add(BinaryTreeNode node, int item, ref bool isUpdated)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(isUpdated == false);

            Contract.Ensures(_root == Contract.OldValue(_root));
            Contract.Ensures(node == null ? ChangeStamp == Contract.OldValue(ChangeStamp) + 1 : true);
            Contract.Ensures(isUpdated ? ChangeStamp == Contract.OldValue(ChangeStamp) + 1 : ChangeStamp == Contract.OldValue(ChangeStamp));
            Contract.Ensures(this.Count >= Contract.OldValue(this.Count));
            Contract.Ensures(Contract.Result<BinaryTreeNode>() != null);
            Contract.Ensures(item == Contract.OldValue(item));
            Contract.Ensures(_hasSnapshot == Contract.OldValue(_hasSnapshot));
            ////Contract.Ensures(_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) : true);
            ////Contract.Ensures(!_hasSnapshot && isUpdated && node != null ? Count == Contract.OldValue(Count) + 1 : true);
            ////Contract.Ensures(!_hasSnapshot && isUpdated && node == null ? Count == Contract.OldValue(Count) : true;
            ////Contract.Ensures(!isUpdated ? Count == Contract.OldValue(Count) : true);

            #endregion

            if (node == null)
            {
                isUpdated = true;
                ChangeStamp++;

                return new BinaryTreeNode(item);
            }

            node = AddMoveDown(node, item, ref isUpdated);

            return node;
        }

        /// <summary>
        /// The part of the add method, where one is moving down the binary tree and back up.
        /// </summary>
        /// <param name="node">
        /// The node.
        /// </param>
        /// <param name="item">
        /// The item.
        /// </param>
        /// <param name="isUpdated">
        /// The is Updated.
        /// </param>
        /// <returns>
        /// The add move down.
        /// </returns>
        private BinaryTreeNode AddMoveDown(BinaryTreeNode node, int item, ref bool isUpdated)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(node != null);
            Contract.Requires(!isUpdated);

            Contract.Ensures(_root == Contract.OldValue(_root));
            Contract.Ensures(item == Contract.OldValue(item));
            Contract.Ensures(_hasSnapshot == Contract.OldValue(_hasSnapshot));

            Contract.Ensures(Count >= Contract.OldValue(Count));
            ////Contract.Ensures(_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) : true);
            ////Contract.Ensures(!_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) + 1 : true);
            ////Contract.Ensures(!isUpdated ? Count == Contract.OldValue(Count) : true);
            
            Contract.Ensures(Contract.Result<BinaryTreeNode>() != null);
            Contract.Ensures(node != null);
            Contract.Ensures(isUpdated ? ChangeStamp == Contract.OldValue(ChangeStamp) + 1 : ChangeStamp == Contract.OldValue(ChangeStamp));

            #endregion

            var cmp = item.CompareTo(node.Item);
            if (cmp < 0)
            {
                var newLeft = Add(node.Left, item, ref isUpdated);
                node = AddMoveleft(node, newLeft, ref isUpdated);
                return node;
            }

        	if (cmp > 0)
        	{
        		var newRight = Add(node.Right, item, ref isUpdated);
        		node = AddMoveRight(node, newRight, ref isUpdated);
        		return node;
        	}

        	return node;
        }

        /// <summary>
        /// Checks if a snapshot has been made and if the add method has inserted the item, if so then a new path
        /// through the tree will be made.
        /// </summary>
        /// <param name="node">
        /// The node.
        /// </param>
        /// <param name="newLeft">
        /// The new Left.
        /// </param>
        /// <param name="isUpdated">
        /// The is Updated.
        /// </param>
        /// <returns>
        /// The add move left.
        /// </returns>
        private BinaryTreeNode AddMoveleft(BinaryTreeNode node, BinaryTreeNode newLeft, ref bool isUpdated)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(node != null);
            Contract.Requires(newLeft != null);

            Contract.Ensures(Count >= Contract.OldValue(Count));
            Contract.Ensures(node != null);
            Contract.Ensures(_root == Contract.OldValue(_root));
            Contract.Ensures(Contract.OldValue(newLeft) == newLeft);
            Contract.Ensures(ChangeStamp == Contract.OldValue(ChangeStamp));
            Contract.Ensures(isUpdated == Contract.OldValue(isUpdated));
            Contract.Ensures(_hasSnapshot == Contract.OldValue(_hasSnapshot));

            ////Contract.Ensures(_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) : true);
            ////Contract.Ensures(!_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) + 1 || Count == Contract.OldValue(Count) : true);
            ////Contract.Ensures(!isUpdated ? Count == Contract.OldValue(Count) : true);
            
            #endregion

            if (_hasSnapshot && isUpdated)
                node = new BinaryTreeNode(newLeft, node.Item, node.Right);
            else
                node.Left = newLeft;

            return node;
        }

        /// <summary>
        /// Checks if a snapshot has been made and if the add method has inserted the item, if so then a new path
        /// through the tree will be made.
        /// </summary>
        /// <param name="node">
        /// The node.
        /// </param>
        /// <param name="newRight">
        /// The new Right.
        /// </param>
        /// <param name="isUpdated">
        /// The is Updated.
        /// </param>
        /// <returns>
        /// The add move right.
        /// </returns>
        private BinaryTreeNode AddMoveRight(BinaryTreeNode node, BinaryTreeNode newRight, ref bool isUpdated)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Requires(node != null);
            Contract.Requires(newRight != null);

            Contract.Ensures(Count >= Contract.OldValue(Count));
            Contract.Ensures(node != null);
            Contract.Ensures(_root == Contract.OldValue(_root));
            Contract.Ensures(Contract.OldValue(newRight) == newRight);
            Contract.Ensures(ChangeStamp == Contract.OldValue(ChangeStamp));
            Contract.Ensures(isUpdated == Contract.OldValue(isUpdated));
            Contract.Ensures(_hasSnapshot == Contract.OldValue(_hasSnapshot));

            ////Contract.Ensures(_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) : true);
            ////Contract.Ensures(!_hasSnapshot && isUpdated ? Count == Contract.OldValue(Count) + 1 || Count == Contract.OldValue(Count) : true);
            ////Contract.Ensures(!isUpdated ? Count == Contract.OldValue(Count) : true);
            
            #endregion);

            if (_hasSnapshot && isUpdated)
                node = new BinaryTreeNode(node.Left, node.Item, newRight);
            else
                node.Right = newRight;

            return node;
        }

        /// <summary>
        /// Determines whether the <see cref="T:System.Collections.Generic.ICollection`1"/> contains a specific value.
        /// </summary>
        /// <returns>
        /// true if <paramref name="item"/> is found in the <see cref="T:System.Collections.Generic.ICollection`1"/>; otherwise, false.
        /// </returns>
        /// <param name="item">The object to locate in the <see cref="T:System.Collections.Generic.ICollection`1"/>.</param>
        [Pure]
        public override bool Contains(int item)
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Ensures(Count == 0 ? Contract.Result<bool>() == false : true);
            Contract.Ensures(Contract.Result<bool>() ? this.Count > 0 : true);

            #endregion

            var node = _root;
            while (node != null)
            {
                if (ContainsCompare(item, ref node))
                    return true;
            }

            return false;
        }

        /// <summary>
        /// Compares a nodes item with an items.
        /// </summary>
        /// <param name="item">
        /// The item.
        /// </param>
        /// <param name="node">
        /// The node.
        /// </param>
        /// <returns>
        /// Returns true if both items are equal. Else go down the tree.
        /// </returns>
        private bool ContainsCompare(int item, ref BinaryTreeNode node)
        {
            #region Code Contracs: Pre - and Post conditions

        	Contract.Requires(this.Count > 0);

            Contract.Ensures(Contract.Result<bool>() ? node != null : true);
            ////Contract.Ensures(_root != null);
            Contract.Ensures(this.Count > 0);

            #endregion

            var cmp = item.CompareTo(node.Item);
            if (cmp < 0)
            {
                node = node.Left;
                return false;
            }

            if (cmp > 0)
            {
                node = node.Right;
                return false;
            }

            return true;
        }

        /// <summary>
        /// Removes all items from the <see cref="T:System.Collections.Generic.ICollection`1"/>.
        /// </summary>
        /// <exception cref="T:System.NotSupportedException">The <see cref="T:System.Collections.Generic.ICollection`1"/> is read-only. </exception>
        public override void Clear()
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Ensures(_root == null);

            #endregion

            _root = null;

            // The following is needed to prove that count indeed will be 0 when root is null
            Contract.Assert(Count == 0);
        }

        /// <summary>
        /// Copies the elements of the <see cref="T:System.Collections.Generic.ICollection`1"/> to an <see cref="T:System.Array"/>, starting at a particular <see cref="T:System.Array"/> index.
        /// </summary>
        /// <param name="array">The one-dimensional <see cref="T:System.Array"/> that is the destination of the elements copied from <see cref="T:System.Collections.Generic.ICollection`1"/>. The <see cref="T:System.Array"/> must have zero-based indexing.</param><param name="arrayIndex">The zero-based index in <paramref name="array"/> at which copying begins.</param><exception cref="T:System.ArgumentNullException"><paramref name="array"/> is null.</exception><exception cref="T:System.ArgumentOutOfRangeException"><paramref name="arrayIndex"/> is less than 0.</exception><exception cref="T:System.ArgumentException"><paramref name="array"/> is multidimensional.-or-The number of elements in the source <see cref="T:System.Collections.Generic.ICollection`1"/> is greater than the available space from <paramref name="arrayIndex"/> to the end of the destination <paramref name="array"/>.</exception>
        public override void CopyTo(int[] array, int arrayIndex)
        {
			Contract.Requires(array != null);
			Contract.Requires(arrayIndex >= 0);
			Contract.Requires(arrayIndex + Count <= array.Length);
			Contract.Requires(arrayIndex + Count > arrayIndex);

        	var list = GetEnumerator();
			while (list.MoveNext())
        	{
        		var current = list.Current;
        		array[arrayIndex++] = current;
        	} 
		}

        /// <summary>
        /// Removes the first occurrence of a specific object from the <see cref="T:System.Collections.Generic.ICollection`1"/>.
        /// </summary>
        /// <returns>
        /// true if <paramref name="item"/> was successfully removed from the <see cref="T:System.Collections.Generic.ICollection`1"/>; otherwise, false. This method also returns false if <paramref name="item"/> is not found in the original <see cref="T:System.Collections.Generic.ICollection`1"/>.
        /// </returns>
        /// <param name="item">The object to remove from the <see cref="T:System.Collections.Generic.ICollection`1"/>.</param><exception cref="T:System.NotSupportedException">The <see cref="T:System.Collections.Generic.ICollection`1"/> is read-only.</exception>
        public override bool Remove(int item)
        {
            throw new NotImplementedException();
        }

        /// <summary>
        /// Gets the number of elements contained in the <see cref="T:System.Collections.Generic.ICollection`1"/>.
        /// </summary>
        /// <returns>
        /// The number of elements contained in the <see cref="T:System.Collections.Generic.ICollection`1"/>.
        /// A sitenote, properties->get is assumed pure from the contracts side. [Pure] attribute are not needed here.
        /// </returns>
        [Pure]
        public override int Count
        {
            get
            {
                Contract.Ensures((_root == null) || (Contract.Result<int>() > 0));
                Contract.Ensures((_root != null) || (Contract.Result<int>() == 0));
                Contract.Ensures(_root == null ? Contract.Result<int>() == 0 : Contract.Result<int>() > 0);
                Contract.Ensures(Contract.Result<int>() >= 0);
                Contract.Ensures(_root == null ? Contract.Result<int>() == 0 : Contract.Result<int>() == CountChildren(_root.Left) + 1 + CountChildren(_root.Right));

                return CountChildren(_root);
            }
        }

        /// <summary>
        /// Count all node from and with the given node.
        /// </summary>
        /// <param name="node">Node from where to count.</param>
        /// <returns>The count.</returns>
        [Pure]
        private static int CountChildren(BinaryTreeNode node)
        {
            Contract.Ensures((node == null) || (Contract.Result<int>() > 0));
            Contract.Ensures((node != null) || (Contract.Result<int>() == 0));
            Contract.Ensures(Contract.Result<int>() >= 0);
            Contract.Ensures(node == null ? Contract.Result<int>() == 0 : Contract.Result<int>() == CountChildren(node.Left) + 1 + CountChildren(node.Right));

            int res;
            if (node == null)
                res = 0;
            else
                res = CountChildren(node.Left) + 1 + CountChildren(node.Right);
            return res;
        }

        /// <summary>
        /// Gets a value indicating whether the <see cref="T:System.Collections.Generic.ICollection`1"/> is read-only.
        /// </summary>
        /// <returns>
        /// true if the <see cref="T:System.Collections.Generic.ICollection`1"/> is read-only; otherwise, false.
        /// </returns>
        public override bool IsReadOnly
        {
            get { return _isSnapshot; }
        }

        #endregion

        #region Implementation of ITree<int>

        /// <summary>
        /// Returns a snapshot of the tree, if the tree isn't already a snapshot itself. Else it will throw an exception!
        /// </summary>
        /// <returns>
        /// A snapshot of the tree, if the tree isn't already a snapshot itself.
        /// </returns>
        public override ITree<int> Snapshot()
        {
            #region Code Contracs: Pre - and Post conditions

            Contract.Ensures(_hasSnapshot);

            #endregion

            _hasSnapshot = true;
            return new A1B1Tree(this);
        }

        /// <summary>
        /// Returns the item for the index i.
        /// </summary>
        /// <param name="index">
        /// The index.
        /// </param>
        /// <returns>
        /// The item for the index i.
        /// </returns>
        public override int GetItem(int index)
		{
			Contract.Requires(index >= 0 && index < Count);
			
            return Get(_root, index);
        }

        /// <summary>
        /// Helper method for Get(int index).
        /// </summary>
        /// <param name="node">
        /// The node.
        /// </param>
        /// <param name="index">
        /// The index.
        /// </param>
        /// <returns>
        /// The index of the node
        /// </returns>
        private int Get(BinaryTreeNode node, int index)
        {
			Contract.Requires(index >= 0 && index < Count);

            var leftCount = CountChildren(node.Left); // Throws if set empty
            while (index != leftCount)
            {
                if (index < leftCount)
                    node = node.Left; // Doesn't throw 
                else
                {
                    // i > leftCount
                    node = node.Right; // Doesn't throw
                    index = index - leftCount - 1;
                }

                leftCount = CountChildren(node.Left); // Throws if i out of range
            }

            return node.Item; // Doesn't throw
        }

        #endregion

		/// <summary>
		/// The customized implementation of ToString
		/// </summary>
		/// <returns>
		/// A string representing all nodes and the structure of the tree.
		/// </returns>
		public override string ToString()
		{
			return _root == null ? "[_]" : _root.ToString();
		}
    }
}